Dieser Audiobeitrag wird von der Universität Erlangen-Nürnberg präsentiert.

Ja, herzlich willkommen zur letzten Sitzung vor Weihnachten. Wir bleiben jetzt erstmal

bei unserem Ansatz uns mit unserer neuen komplizierteren Logik erstmal rein

syntaktisch auseinanderzusetzen. Und zwar vergessen wir sogar die Formeln jetzt

erstmal wieder für einen Moment und beschäftigen uns allein mit Termen.

Konkret mit einem wichtigen algorithmischen Problem auf Termen, nämlich

nämlich mit Unifikationen. Ja, was das Unifikationsproblem ist, lässt sich

relativ schnell sagen. Das hat als Input einfach zwei Terme. Im einfachen Fall, wir

werden es nachher etwas allgemeiner formulieren. Und die Frage ist, existiert

eine Substitution Sigma? Ja, also Sigma ist unser reservierter Buchstabe für

Substitutionen, bzw. wollen wir so einen Sigma dann auch finden, das folgende

Eigenschaft hat. Wir wollen, dass die beiden Terme gleich werden, wenn wir eben

links und rechts diese Substitutionen ausführen. Und mit gleich meinen wir

syntaktisch gleich. Also nicht irgendwie gleich moduloiriririririririririririririririririririririririririririririrr

Wir wollen das gleich kriegen ohne, dass wir wissen was da stattfindet. Also

dass da zum Beispiel irgendwelche Gesetze für Additionen gelten oder so was.

Sondern wir wollen, dass das syntaktisch gleiche Terme werden. So irgendwo haben

wir hier ein Beispiel.

Also hier ein ganz primitives Beispiel.

E wäre also dieser linke Term hier, f von g von x und rechts das D wäre einfach f von

y.

Nun haben wir keine Schwierigkeiten, eine Lösung zu finden.

Das sieht man so halb über den Daumen gepeilt.

Also da können wir nehmen die Substitution, die einfach y durch g von x ersetzt.

Wenn wir das tun, dann passiert auf der linken Seite gar nichts, auf der rechten Seite kommt

f von g von x raus.

Also sind taktisch gleiche Terme und wir brauchen da also über f und g nichts weiter zu wissen,

was die tun.

Ja sind taktisch gleiche Terme liefern sicher gleiche Ergebnisse.

Fine.

So, das klingt nach einem primitiven Problem.

Es wird sich als algorithmisch doch relativ herausfordernd herausstellen.

Insbesondere die Analyse des Algorithmus ist da nicht völlig trivial und das ist ja nur

die Grundversion hier, wo wir also einen sehr einfachen Begriff von Termen haben, wo wir

einfach nur so Operatoren aufeinander stapeln.

Also wer kann HESCAL?

Okay, sind relativ wenige.

Ja, also HESCAL hat so eine Lambda Notation, die wir oder wer kann LISP?

Das können vielleicht noch mehr.

Verdammt wenig.

Wer kann irgendeine funktionale Sprache?

ML.

Ja, was kann man denn heutzutage?

Was?

Scala.

Ja, okay.

Scala hat das glaube ich auch.

Also Scala hat auch ein Lambda glaube ich.

Ja, also wenn man also so einen Bindungsoperator hat, das lernen wir in TH-Proc noch genauer

kennen, dann hat man auch einen Begriff von Termen und kann darauf auch ein Unifikationsproblem